(cl-text ConnectorType1and2
(cl-comment "ConnectorType
			[1and2] Given a port, all connectors should lead to classes that are subtypes of the port (except connectors between port.isConjugated and part, when type does not care)")
(forall (p)   
		(if
			(cbuml:Port p)
			(and 
				(form:port-covers-assemblies p)
				(form:port-covers-delegations p)
				)
	     )
	)
)

(cl-text ConnectorType3
(cl-comment "ConnectorType
			[3] Given a port not conjugated, all connected delegation connectors should lead to classes that together are pairwise disjoint (not ambiguous) or be active")
(forall (p t)   
		(if
			(and
				(cbuml:Port p)
				(buml:type p t)
				(not (cbuml:isConjugated p form:true))
				)
			(or
				(cbuml:isActive t form:true)
				(not (exists (t1 t2)
					(form:port-ambiguous-delegation p t1 t2 )
				))		
			)
	     )
	)
)


(cl-text ConnectorType4
(cl-comment "Connector
			[4] Given a port conjugated, all connected assembly connectors should lead to classes that together are pairwise disjoint (not ambiguous) or be active")
(forall (p t)   
		(if
			(and
				(cbuml:Port p)
				(buml:type p t)
				(cbuml:isConjugated p form:true)
				)
			(or
				(cbuml:isActive t form:true)
				(not (exists (t1 t2)
					(form:port-ambiguous-assembly p t1 t2 )
				))		
			)
	     )
	)
)